1. Technical Field
This disclosure generally relates to formal verification. More specifically, this disclosure relates to formal verification of bit-serial division and bit-serial square root circuit designs.
2. Related Art
The importance of circuit verification cannot be over-emphasized. Indeed, without circuit verification it would have been practically impossible to design complicated integrated circuits (ICs) which are commonly found in today's computing devices.
Circuits that perform division and that compute a square root are used extensively in ICs. For example, these circuits are commonly used in central processing units (CPUs), graphics processors, digital signal processors, etc. There have been many cases in which a bug in a circuit implementation of a mathematical operator had a significant impact on the company's finances. For example, in one well-publicized instance, a bug in a floating-point division circuit cost the company hundreds of millions of dollars. Therefore, it is very important to guarantee that certain circuits (e.g., division and square root circuits) in an IC will operate correctly.
One approach to verify a circuit design is to exhaustively simulate the circuit design. However, this approach is clearly impractical because it is computationally infeasible (and often impossible) to exhaustively simulate non-trivial circuit designs such division circuit designs and square-root circuit designs.
Another approach uses formal verification to prove correctness of a circuit design. Unfortunately, naïve formal verification based approaches can have serious runtime and memory issues when they are used to prove correctness of division and square-root circuit designs. Hence, what is needed are techniques and systems for formally verifying division and square-root circuit designs without the above-described problems.